\documentclass{article}
\usepackage{amsmath,amssymb,fouriernc,parskip,amsthm}
\usepackage{hyperref}
\hypersetup{
  citecolor=red,
  colorlinks=true
}
\title{Fixed Point}
\date{}
\author{}
\begin{document}
\theoremstyle{definition}
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}
\newtheorem{defn}[thm]{Definition}

\maketitle

Fix a valid fixed point format $fmt$, and let $Fixed$ be the set of all 
fixed point numbers in this format (i.e., the set of all real numbers $x$ for 
which $is\_fixed(fmt,x)$ is true).

\section{Rounding}

\begin{lem}
\label{fixedfinite}
\begin{equation*}
FINITE(Fixed)
\end{equation*}
\begin{proof} Let $I = \{0, 1, \ldots, 2r^{p - 1} - 1\}$. $I$ is finite 
(FINITE\_NUMSEG). Let
\begin{equation*}
f(i) = \left \{
\begin{array}{ll}
0 & \text{if $i = 0$}\\
(i + 1)/2 \cdot r^{e - p + 1} & \text{if $i$ is odd}\\
i/2 \cdot r^{e - p + 1} & \text{if $i$ is even}
\end{array} \right .
\end{equation*}
Let $s \in Fixed$; then $|s| = f \cdot r^{e - p + 1}$ and $0 \leq f < r^{p - 1}$.
If $s = 0$, $s = f(0)$. If $s > 0$, $f > 0$, and $s = f(2f - 1)$. If $s < 0$,
then $f > 0$, and $s = f(2f)$.

We have shown $Fixed \subset f(I)$. $Fixed$ is therefore finite. (FINITE\_IMAGE)
\end{proof}
\end{lem}

\begin{defn}
\label{bounds}
For any $x \in \mathbb{R}$, let
\begin{align*}
S_x^- &= \{ \; s \in Fixed \; | \; s \leq x \; \}\\
S_x^+ &= \{ \; s \in Fixed \; | \; s \geq x \; \}
\end{align*}
and $x^- = \sup{\big ( \; S_x^- \; \big )}$, $x^+ = \inf{\big ( \; S_x^+ \; 
\big )}$.
\end{defn}

\begin{lem}
\label{distance}
\begin{equation*}
\forall u, v \in Fixed \; . \; u \leq v \; \wedge \; v \leq u + fulp \;
\Longrightarrow \; v = u \; \vee \; v = u + fulp
\end{equation*}
\begin{proof} Assume the antecedent, so we have $u \leq v \leq u + fulp$.
Suppose the goal is not true. Then in fact
\begin{equation*}
u < v < u + fulp 
\end{equation*}
which implies
\begin{equation*}
ff(u) \cdot r^{e - p + 1} < ff(v) \cdot r^{e - p + 1} < (ff(u) + 1) \cdot r^{e - p + 1}
\end{equation*}
Dividing by the non-zero $r^{e - p + 1}$ gives
\begin{equation*}
ff(u) < ff(v) < ff(u) + 1
\end{equation*}
a contradiction, as the fractions are natural numbers.
\end{proof}
\end{lem}

\begin{lem}
\label{bounddistance}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \; x^- \leq x^+ \; \wedge \; x^+ \leq x^- + fulp
\end{equation*}
\begin{proof} Assume the antecedent. Since $|x| \leq finf$, $S_x^-$ and
$S_x^+$ are non-empty (they contain $-finf$ and $finf$ respectively).
Hence, $x^-$ and $x^+$ are maximal and minimal elements of $S_x^-$ and
$S_x^+$, respectively (SUP\_UNIQUE\_FINITE).

Let $s = x^- + fulp > x^-$. $s$ is a fixed point number with fraction
$ff(x^-) + 1$. Either $s \leq x$ or $s \geq x$. If $s \leq x$, then
$s \leq x^-$ by defn of $x^-$, which is impossible. If $s \geq x$, then
$s \geq x^+$.
\end{proof}
\end{lem}

\begin{lem}
\label{bounddistance2}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \; x^+ = x^- \; \vee \; x^+ = x^- + fulp
\end{equation*}
\begin{proof} Simple combination of ~\ref{distance} and ~\ref{bounddistance}.
\end{proof}
\end{lem}

\begin{lem}
\label{boundbetw}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \; 
\forall s \in Fixed \; . \; s \leq x^- \; \vee \; s \geq x^+
\end{equation*}
\begin{proof} Assume the antecedent. Suppose, for a contradiction, that
there is some $s$ with $s > x^-$ and $s < x^+$. Then $s \geq x^-$ and
$s \leq x^+ \leq x^- + fulp$ from ~\ref{bounddistance2}. It then follows
from ~\ref{distance} that $s = x^-$ or $s = x^- + fulp$, both contradictions.
\end{proof}
\end{lem}

\begin{thm}
\label{rndnear}
\begin{align*}
&\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \\
& \quad \Big [ \; \forall s^* \in Fixed \; . \; s^* = round(to\_nearest,x) \; 
\Longleftrightarrow \\
& \quad \Big [ \; \forall s' \in Fixed \; . \; 
\neg closer(s^*, s', x) \; 
\Longrightarrow
\; \big(\neg closer(s', s^*, x) \; \wedge \; even(ff(s^*)) \big) \; \Big ]
\; \Big ]
\end{align*}
\begin{proof} Assume the antecedent. $round(to\_nearest,x)$ is either
$x^-$ or $x^+$, with the corresponding assumptions and properties
(SUP\_UNIQUE\_FINITE again).

Suppose $round(to\_nearest, x) = x^-$, so $s^* = x^-$. 

Suppose $closer(x^-, x^+,x)$ is true. Suppose there is an $s' \in Fixed$
with $\neg closer(s^*, s', x)$. If $s' = x^-$, contradiction. If
$s' = x^+$, contradiction. Otherwise, from ~\ref{boundbetw}, $s' < x^-$
or $s' > x^+$. In either case, contradiction (I'm assuming arith rule
can take over here).

Suppose $closer(x^-, x^+,x)$ is false, but $ff(x^-)$ is true, so
again $s^* = x^-$. Suppose there is an $s' \in Fixed$
with $\neg closer(s^*, s', x)$. If $s' = x^-$, contradiction. If
$s' = x^+$, then $\neg closer(s', s^*, x)$ and $ff(s^*)$; OK. Otherwise, 
from ~\ref{boundbetw}, $s' < x^-$ or $s' > x^+$. In either case, contradiction.

The proof is similar for $x^+$.
\end{proof}
\end{thm}

The proofs for other rounding modes are similar.

\begin{thm}
\label{abserror}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \; \Longrightarrow \;
|round(to\_nearest, x) - x| \leq fulp/2
\end{equation*}
\begin{proof} Assume the antecedent. Since $|x| \leq finf$, 
$x^-$ and $x^+$ have the desired property that $x^- \leq x$ and
$x \leq x^+$.

Suppose $round(to\_nearest,x) = x^-$ (with the corresponding assumptions).
Either $x > x^-$ or $x = x^-$. If $x = x^-$, the error is zero. If $x > x^-$,
then $x^- < x \leq x^+$ and $|x^- - x| \leq |x^+ - x|$ (defn of closer). 
It then follows (I'm thinking arith tac can do it) that 
$|x^-  - x| \leq |x^+ - x^-| / 2$. From ~\ref{bounddistance}, 
$|x^+ - x^-| \leq fulp$, whence $|x^- - x| \leq fulp/2$.

The proof for $x^+$ is similar.
\end{proof}
\end{thm}

The proof for the other rounding modes is similar, but easier, and the
bound on the absolute error is $fulp$ instead of $fulp/2$.

\begin{lem}
\label{rnddown}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \;
\big [ \; x < x^- + fulp/2 \; \Longrightarrow \; round(to\_nearest, x) = x^-
\; \big ]
\end{equation*}
\begin{proof} Assume the antecedent. Then $x^-$ and $x^+$ exist with the
desired properties. From ~\ref{bounddistance2}, $x^+ = x^-$ or $x^+ =
x^- + fulp$. If $x^+ = x^-$, then no matter what, $round(to\_nearest,x)$
rewrites to $x^-$.

Suppose $x^+ = x^- + fulp$. It then follows that
\begin{equation*}
x - x^- < fulp/2 = (x^+ - x^-)/2
\end{equation*}
and hence (arith tac?) $x - x^- < x^+ - x$, or $|x - x^-| < |x^+ - x|$. 
Therefore, $closer(x^-, x^+, x)$, and $round(to\_nearest, x) = x^-$ 
(probably some extra steps here in HOL light).
\end{proof}
\end{lem}

\begin{lem}
\label{rndup}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \;
\Longrightarrow \;
\big [ \; x > x^- + fulp/2 \; \Longrightarrow \; round(to\_nearest, x) = x^+
\; \big ]
\end{equation*}
\begin{proof} Similar proof.
\end{proof}
\end{lem}

\begin{thm}
\label{relerror}
\begin{equation*}
\forall x \in \mathbb{R} \; . \; |x| \leq finf \; \wedge \; x \neq 0 \;
\Longrightarrow \;
\left | \frac{round(to\_nearest, x) - x}{x} \right | \leq 1
\end{equation*}
\begin{proof} Assume the antecedent. Either $0 < |x| \leq fulp/2$ or 
$|x| > fulp/2$. If $0 < |x| \leq fulp/2$, then $-fulp/2 \leq x \leq fulp/2$.
It then follows from ~\ref{rnddown} and ~\ref{rndup} with $x^- = 0$ and
$x^+ = 0$ (depending on the case) that $round(to\_nearest,x) = 0$, and so
\begin{equation*}
\left | \frac{round(to\_nearest, x) - x}{x} \right | = 1
\end{equation*}
Suppose $|x| > fulp/2$. Since $|x| \leq finf$, from
~\ref{abserror} we have
\begin{equation*}
\left | round(to\_nearest, x) - x \right | \leq fulp/2
\end{equation*}
It then follows that
\begin{equation*}
\left | \frac{round(to\_nearest, x) - x}{x} \right | 
\leq \frac{fulp/2}{|x|} \leq 1
\end{equation*}
\end{proof}
\end{thm}

\end{document}
